poss:(ES{i}{i'}), T:Type{i}, s:T, i:Id, P:(possible-event{i:l}(poss){i'}),
R:(possible-event{i:l}(poss)possible-event{i:l}(poss){i'}), Rs:(TT{i'}).
ma-knows{i:l}(poss; i; T; s; P; Rs; R)  {i'} 

latex

Definitions	Ki(P)@s, P  Q, poss-consistent(i;T;s;ev;R), K(P)@e, PossibleEvent(poss), x:A. B(x), Id, x:AB(x), ES, t  T, , Type
Lemmas	event system wf, Id wf, possible-event wf, es-knows wf, poss-consistent wf